/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.util.Arrays;
import java.util.List;

import alloy.bool.BooleanFormula;
import alloy.bool.PartialAssignment;

/** Translation of a {@link alloy.ast.Formula}. */
public class FormulaTransl extends Transl {
    public BooleanFormula formula;

    /**
     * These singleton fields hold mutable state, so they should be re-initialized for each compile.
     * They should only be set by the initSingletons() method.
     */
    private static /*final*/ FormulaTransl FALSE = null; //new FormulaTransl(BooleanFormula.FALSE());
    private static /*final*/ FormulaTransl TRUE = null; // new FormulaTransl(BooleanFormula.TRUE());

	static FormulaTransl FALSE() { return FALSE; }
    static FormulaTransl TRUE() { return TRUE; }

    /**
     * Should be called before each compile.
     *
     */
    public static void initSingletons() {
    	BooleanFormula.initSingletons();    	// we need to make sure that this gets called first
    	FALSE = new FormulaTransl(BooleanFormula.FALSE());
        TRUE = new FormulaTransl(BooleanFormula.TRUE());    
    }
    
    
	public FormulaTransl(BooleanFormula formula_) {
		if (formula_ == null) throw new NullPointerException();
		this.formula = formula_; 
	}
    
	public List getBooleanFormulas() { return Arrays.asList(new Object[]{formula}); }
    public FormulaTransl and(FormulaTransl otherFT_) { return new FormulaTransl(formula.and(otherFT_.formula)); }
    public FormulaTransl or(FormulaTransl otherFT_) { return new FormulaTransl(formula.or(otherFT_.formula)); }
    public FormulaTransl iff(FormulaTransl otherFT_) { return new FormulaTransl(formula.iff(otherFT_.formula)); }
    public FormulaTransl not() { return new FormulaTransl(formula.not()); }
    public FormulaTransl implies(FormulaTransl otherFT_) { return new FormulaTransl(formula.implies(otherFT_.formula)); }

    public void simplify(PartialAssignment pa_) { formula = formula.simplify(pa_); }

    public String interpret(boolean[] assignment_) {
	return formula.interpret(assignment_) ? "T" : "F";
    }
}

